((LIST ((((∀ U V)) (= (* U V) (CONDI (NULL U) V (CONS (CAR U) (* (CDR U) V))))) . (AXIOM (TM& ((∀ U V)) (= (* U V) (CONDI (NULL U) V (CONS (CAR U) (* (CDR U) V)))))) . NIL . ((* LISP . 18) (U . (VARIABLE . (VAR& . VTYP1) . UNIVERSAL . NIL . NIL . 1 . U .)) (V . (VARIABLE . (VAR& . VTYP2) . UNIVERSAL . NIL . NIL . 1 . V .)) (NULL . (VARIABLE . (VAR& . VTYP3) . UNIVERSAL . NIL . NIL . 1 . NULL .)) (CONS . (VARIABLE . (VAR& . VTYP4) . UNIVERSAL . NIL . NIL . 1 . CONS .)) (CAR . (VARIABLE . (VAR& . VTYP5) . UNIVERSAL . NIL . NIL . 1 . CAR .)) (CDR . (VARIABLE . (VAR& . VTYP6) . UNIVERSAL . NIL . NIL . 1 . CDR .))) . NIL . ((VTYP6 (GROUND) . GROUND) (VTYP3 (GROUND) . TRUTHVAL) (VTYP2 . GROUND) (VTYP1 . GROUND) (VTYP5 (GROUND) VAR& . VTYP8) (VTYP4 ((VAR& . VTYP8) GROUND) VAR& . VTYP10)) . NIL . (1) . NIL . LIST . NIL . NIL . 1 .)) (COPY (NIL . (DECL (COPY) (OT& (GROUND) . GROUND) CONSTANT) . NIL . ((COPY . (CONSTANT . ((GROUND) . GROUND) . UNIVERSAL . NIL . NIL . 1 . COPY .))) . NIL . NIL . NIL . NIL . NIL . COPY . NIL . NIL . 1 .) ((((∀ U)) (= (COPY U) (CONDI (NULL U) NNIL (CONS (CAR U) (COPY (CDR U)))))) . (AXIOM (TM& ((∀ U)) (= (COPY U) (CONDI (NULL U) NNIL (CONS (CAR U) (COPY (CDR U))))))) . NIL . ((U LISP . 1) (NNIL LISP . 5) (CONS LISP . 6) (CAR LISP . 7) (CDR LISP . 7) (NULL LISP . 8) (COPY . 1)) . NIL . NIL . NIL . (2) . NIL . COPY . NIL . NIL . 2 .) ((⊃ (∧ (= (COPY NNIL) NNIL) (((∀ X U)) (⊃ (= (COPY U) U) (= (COPY (CONS X U)) (CONS X U))))) (((∀ U)) (= (COPY U) U))) . (∀E PHI (TM& ((λ V)) (= (COPY V) V)) (LN& LISP . 17) (LR& (LISP . 12))) . NIL . ((U LISP . 1) (X LISP . 2) (NNIL LISP . 5) (CONS LISP . 6) (COPY . 1)) . NIL . NIL . NIL . ((LISP . 17) (LISP . 12)) . NIL . COPY . NIL . NIL . 3 .) ((((∀ X U)) (= (COPY (CONS X U)) (CONS X (COPY U)))) . (DECSIMP (TM& ((∀ X U)) (= (COPY (CONS X U)) (CONS X (COPY U)))) SRIGHT (LR&) (LR&) (LR& (LISP . 12)) (LR& 2 (LISP . 14) (LISP . 15) (LISP . 16))) . NIL . ((COPY . 1) (U LISP . 1) (X LISP . 2) (CONS LISP . 6)) . NIL . NIL . NIL . ((LISP . 16) (LISP . 15) (LISP . 14) 2 (LISP . 12)) . NIL . COPY . NIL . NIL . 4 .) ((((∀ U)) (= (COPY U) U)) . (DECSIMP (TM& ((∀ U)) (= (COPY U) U)) SRIGHT (LR& 3) (LR&) (LR& (LISP . 12)) (LR& 2 (LISP . 13) 4)) . NIL . ((COPY . 1) (U LISP . 1)) . NIL . NIL . NIL . ((LISP . 12) 2 (LISP . 14) (LISP . 15) (LISP . 16) (LISP . 13) (LISP . 17)) . NIL . COPY . NIL . NIL . 5 .)) (LISP (NIL . (DECL (U V W) (OT& . GROUND) VARIABLE LIST) . NIL . ((W . (VARIABLE . GROUND . LIST . NIL . NIL . 1 . W .)) (U . (VARIABLE . GROUND . LIST . NIL . NIL . 1 . U .)) (LIST . (VARIABLE . ((GROUND) . TRUTHVAL) . UNIVERSAL . NIL . (4 . LIST . PREFIX . 1000 .) . 1 . LIST .)) (V . (VARIABLE . GROUND . LIST . NIL . NIL . 1 . V .))) . NIL . NIL . NIL . NIL . NIL . LISP . NIL . NIL . 1 .) (NIL . (DECL (X Y Z) (OT& . GROUND) VARIABLE SEXP) . NIL . ((Z . (VARIABLE . GROUND . SEXP . NIL . NIL . 2 . Z .)) (X . (VARIABLE . GROUND . SEXP . NIL . NIL . 2 . X .)) (SEXP . (VARIABLE . ((GROUND) . TRUTHVAL) . UNIVERSAL . NIL . (4 . SEXP . PREFIX . 1000 .) . 2 . SEXP .)) (Y . (VARIABLE . GROUND . SEXP . NIL . NIL . 2 . Y .))) . NIL . NIL . NIL . NIL . NIL . LISP . NIL . NIL . 2 .) (NIL . (DECL (A B C) (OT& . GROUND) VARIABLE) . NIL . ((C . (VARIABLE . GROUND . UNIVERSAL . NIL . NIL . 3 . C .)) (A . (VARIABLE . GROUND . UNIVERSAL . NIL . NIL . 3 . A .)) (B . (VARIABLE . GROUND . UNIVERSAL . NIL . NIL . 3 . B .))) . NIL . NIL . NIL . NIL . NIL . LISP . NIL . NIL . 3 .) (NIL . (DECL (PHI) (OT& (GROUND) . TRUTHVAL) VARIABLE) . NIL . ((PHI . (VARIABLE . ((GROUND) . TRUTHVAL) . UNIVERSAL . NIL . NIL . 4 . PHI .))) . NIL . NIL . NIL . NIL . NIL . LISP . NIL . NIL . 4 .) (NIL . (DECL (NNIL) (OT& . GROUND) CONSTANT LIST) . NIL . ((NNIL . (CONSTANT . GROUND . LIST . NIL . NIL . 5 . NNIL .)) (LIST . 1)) . NIL . NIL . NIL . NIL . NIL . LISP . NIL . NIL . 5 .) (NIL . (DECL (CONS) (OT& (GROUND GROUND) . GROUND) CONSTANT) . NIL . ((CONS . (CONSTANT . ((GROUND GROUND) . GROUND) . UNIVERSAL . NIL . NIL . 6 . CONS .))) . NIL . NIL . NIL . NIL . NIL . LISP . NIL . NIL . 6 .) (NIL . (DECL (CAR CDR) (OT& (GROUND) . GROUND) CONSTANT) . NIL . ((CDR . (CONSTANT . ((GROUND) . GROUND) . UNIVERSAL . NIL . NIL . 7 . CDR .)) (CAR . (CONSTANT . ((GROUND) . GROUND) . UNIVERSAL . NIL . NIL . 7 . CAR .))) . NIL . NIL . NIL . NIL . NIL . LISP . NIL . NIL . 7 .) (NIL . (DECL (NULL) (OT& (GROUND) . TRUTHVAL) CONSTANT) . NIL . ((NULL . (CONSTANT . ((GROUND) . TRUTHVAL) . UNIVERSAL . NIL . NIL . 8 . NULL .))) . NIL . NIL . NIL . NIL . NIL . LISP . NIL . NIL . 8 .) (NIL . (DECL (LIST) (OT& (GROUND) . TRUTHVAL) CONSTANT) . NIL . ((LIST . (CONSTANT . ((GROUND) . TRUTHVAL) . UNIVERSAL . NIL . NIL . 9 . LIST .))) . NIL . NIL . NIL . NIL . NIL . LISP . NIL . NIL . 9 .) (NIL . (DECL (SEXP) (OT& (GROUND) . TRUTHVAL) CONSTANT) . NIL . ((SEXP . (CONSTANT . ((GROUND) . TRUTHVAL) . UNIVERSAL . NIL . NIL . 10 . SEXP .))) . NIL . NIL . NIL . NIL . NIL . LISP . NIL . NIL . 10 .) ((((∀ U)) (SEXP U)) . (AXIOM (TM& ((∀ U)) (SEXP U))) . NIL . ((U . 1) (SEXP . 10)) . NIL . NIL . NIL . (11) . NIL . LISP . NIL . NIL . 11 .) ((((∀ X U)) (LIST (CONS X U))) . (AXIOM (TM& ((∀ X U)) (LIST (CONS X U)))) . NIL . ((U . 1) (X . 2) (CONS . 6) (LIST . 9)) . NIL . NIL . NIL . (12) . NIL . LISP . NIL . NIL . 12 .) ((((∀ U)) (≡ (NULL U) (= U NNIL))) . (AXIOM (TM& ((∀ U)) (≡ (NULL U) (= U NNIL)))) . NIL . ((U . 1) (NNIL . 5) (NULL . 8)) . NIL . NIL . NIL . (13) . NIL . LISP . NIL . NIL . 13 .) ((((∀ X U)) (¬ (NULL (CONS X U)))) . (AXIOM (TM& ((∀ X U)) (¬ (NULL (CONS X U))))) . NIL . ((U . 1) (X . 2) (CONS . 6) (NULL . 8)) . NIL . NIL . NIL . (14) . NIL . LISP . NIL . NIL . 14 .) ((((∀ X U)) (= (CAR (CONS X U)) X)) . (AXIOM (TM& ((∀ X U)) (= (CAR (CONS X U)) X))) . NIL . ((U . 1) (X . 2) (CONS . 6) (CAR . 7)) . NIL . NIL . NIL . (15) . NIL . LISP . NIL . NIL . 15 .) ((((∀ X U)) (= (CDR (CONS X U)) U)) . (AXIOM (TM& ((∀ X U)) (= (CDR (CONS X U)) U))) . NIL . ((U . 1) (X . 2) (CONS . 6) (CDR . 7)) . NIL . NIL . NIL . (16) . NIL . LISP . NIL . NIL . 16 .) ((((∀ PHI)) (⊃ (∧ (PHI NNIL) (((∀ X U)) (⊃ (PHI U) (PHI (CONS X U))))) (((∀ U)) (PHI U)))) . (AXIOM (TM& ((∀ PHI)) (⊃ (∧ (PHI NNIL) (((∀ X U)) (⊃ (PHI U) (PHI (CONS X U))))) (((∀ U)) (PHI U))))) . NIL . ((U . 1) (X . 2) (PHI . 4) (NNIL . 5) (CONS . 6)) . NIL . NIL . NIL . (17) . NIL . LISP . NIL . NIL . 17 .) (NIL . (DECL (*) (OT& (GROUND GROUND) . GROUND) CONSTANT NIL INFIX 800) . NIL . ((* . (CONSTANT . ((GROUND GROUND) . GROUND) . UNIVERSAL . NIL . (1 . * . INFIX . 800 .) . 18 . * .))) . NIL . NIL . NIL . NIL . NIL . LISP . NIL . NIL . 18 .) ((((∀ U V)) (= (* U V) (CONDI (NULL U) V (CONS (CAR U) (* (CDR U) V))))) . (AXIOM (TM& ((∀ U V)) (= (* U V) (CONDI (NULL U) V (CONS (CAR U) (* (CDR U) V)))))) . NIL . ((* . 18) (U . 1) (V . 1) (NULL . 8) (CONS . 6) (CAR . 7) (CDR . 7)) . NIL . NIL . NIL . (19) . NIL . LISP . NIL . NIL . 19 .) ((((∀ X U V)) (= (* (CONS X U) V) (CONS X (* U V)))) . (DECSIMP (TM& ((∀ X U V)) (= (* (CONS X U) V) (CONS X (* U V)))) SRIGHT (LR&) (LR&) (LR& 12) (LR& 19 14 15 16)) . NIL . ((CONS . 6) (X . 2) (U . 1) (V . 1) (* . 18)) . NIL . NIL . NIL . (16 15 14 19 12) . NIL . LISP . NIL . NIL . 20 .) ((⊃ (∧ (((∀ V)) (LIST (* NNIL V))) (((∀ X U)) (⊃ (((∀ V)) (LIST (* U V))) (((∀ V)) (LIST (* (CONS X U) V)))))) (((∀ U V)) (LIST (* U V)))) . (∀E PHI (TM& ((λ U)) (((∀ V)) (LIST (* U V)))) (LN& . 17) (LR& 12)) . NIL . ((* . 18) (V . 1) (LIST . 9) (U . 1) (X . 2) (NNIL . 5) (CONS . 6)) . NIL . NIL . NIL . (17 12) . NIL . LISP . NIL . NIL . 21 .) ((⊃ (∧ (LIST (* NNIL V)) (((∀ X U)) (⊃ (LIST (* U V)) (LIST (* (CONS X U) V))))) (((∀ U)) (LIST (* U V)))) . (∀E PHI (TM& ((λ U)) (LIST (* U V))) (LN& . 17) (LR& 12)) . NIL . ((U . 1) (X . 2) (NNIL . 5) (CONS . 6) (LIST . 9) (* . 18) (V . 1)) . NIL . NIL . NIL . (17 12) . NIL . LISP . NIL . NIL . 22 .) ((⊃ (((∀ X U)) (⊃ (LIST (* U V)) (LIST (* (CONS X U) V)))) (((∀ U)) (LIST (* U V)))) . (REWRITE SRIGHT (LN& . 22) (LR& 19 13 14 15 16) (LR& 12)) . NIL . ((U . 1) (X . 2) (CONS . 6) (LIST . 9) (* . 18) (V . 1)) . NIL . NIL . NIL . (17 19 13 14 15 16 12) . NIL . LISP . NIL . NIL . 23 .) ((⊃ (((∀ X U)) (⊃ (LIST (* U V)) (LIST (CONS X (* U V))))) (((∀ U)) (LIST (* U V)))) . (REWRITE SRIGHT (LN& . 22) (LR& 20 19 13 14 15 16) (LR& 12)) . NIL . ((U . 1) (X . 2) (CONS . 6) (LIST . 9) (* . 18) (V . 1)) . NIL . NIL . NIL . (17 19 13 14 15 16 12) . NIL . LISP . NIL . NIL . 24 .) ((((∀ U)) (LIST (* U V))) . (TAUT (TM& ((∀ U)) (LIST (* U V))) (LR& 24 12)) . NIL . ((V . 1) (* . 18) (LIST . 9) (U . 1)) . NIL . NIL . NIL . (12 16 15 14 13 19 17) . NIL . LISP . NIL . NIL . 25 .)))